r:rationals. qpositive(r)   

latex

Definitions	gt(i; j), guard(T), sq_type(T), P  Q, prop{i:l}, P  Q, P  Q, P  Q, P  Q, ff, if b then t else f fi , qpositive(r), tt, t  T, x:A. B(x), False, A, decidable(P), qeq(r; s), , int_nzero, b-union(A; B), rationals
Lemmas	iff functionality wrt iff, int entire, decidable int equal, decidable lt, neg mul arg bounds, pos mul arg bounds, gt wf, and functionality wrt iff, assert of band, or functionality wrt iff, assert of bor, iff transitivity, band wf, bor wf, assert wf, assert of eq int, assert of lt int, eqtt to assert, lt int wf, iff imp equal bool, rationals wf, btrue wf, qeq wf, bool wf